T:Type, L:T List, f, g:(||L||||L||). ((L o f) o g) = (L o f o g)  T List 

latex

Definitions	x:A. B(x), (L o f), ij, ||as||, , t  T, {i..j}, P  Q, l[i], P & Q, i  j < k, AB, False, A, P  Q, P  Q, Prop, S  T, S  T, f o g
Lemmas	length wf1, compose wf, permute list length, int seg wf, list extensionality, permute list wf, nat wf, permute list select, le wf, select wf, non neg length